| Definitions | Type, EqDecider(T),  x:A. B(x), P    Q, list_accum(x,a.f(x;a); y; l), l-union(eq; as; bs), P  Q,  x:A. B(x), P  Q, type List, (x  l), left + right, x:A  B(x), x:A  B(x), t T, P Q, guard(T), P Q, False,   x. t(x), x.A(x), x,y. t(x;y), prop{i:l}, cons(car; cdr), A c B, s = t, a < b,  ,  T, True, [], l-union-list(eq; ll), {x:A| B(x)} ,  , A  B,  A, ||as||, Y, rec-case(a) of [] => s | x::y => z.t(x;y;z), n + m, l[i], hd(l), nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), i z j,  b, i <z j, if a<b then c else d, n - m, tl(l) |